package trabajoISW2.domain.contracts;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.Author;
import trabajoISW2.domain.implementations.Publisher;
import trabajoISW2.domain.implementations.Subject;

@Inv({"getIsbn().SIZE == 10 || getIsbn().SIZE ==13"})
public interface IBook {
	


	@Pre({"isbn.length() == 10 || isbn.length() == 13 #IllegalArgumentException", "isbn != null #IllegalArgumentException"})
	@Pos("getIsbn() == isbn")
	public void setIsbn (String isbn);
	
	@Query
	public String getIsbn ();
	
	@Pre({"title.compareTo(\"\") != 0 #WrongNameException", "title != null #WrongNameException"})
	@Pos("getTitle() == title")
	public void setTitle (String title);
	
	@Query
	public String getTitle();
	
	@Pre("price >= 0 && price <= Double.MAX_VALUE #NoPositiveNumberException")
	@Pos("getPrice() == price")
	public void setPrice (double price);
	
	@Query
	public double getPrice();
	
	@Pre({"summary.compareTo(\"\") != 0 #WrongNameException", "summary != null #WrongNameException"})
	@Pos("getSummary() == summary")
	public void setSummary (String summary);
	
	@Query
	public String getSummary();
	
	@Pre({"language.compareTo(\"\") != 0 #WrongNameException", "language != null #WrongNameException"})
	@Pos("getLanguage() == language")
	public void setLanguage (String language);
	
	@Query
	public String getLanguage();
	
	@Pre({"year > 0 #NoPositiveNumberException", "year <= Calendar.getInstance().YEAR #NoPositiveNumberException" })
	@Pos("getYear() == year")
	public void setYear (int year);
	
	@Query
	public int getYear();
	
	@Pre("author != null #IllegalArgumentException")
	@Pos("getAuthor().compare(author) == 0")
	public void setAuthor(Author author);
	
	@Query
	public Author getAuthor();
	
	@Pre({"publisher != null #IllegalArgumentException"})
	@Pos("getPublisher().compare(publisher) == 0")
	public void setPublisher(Publisher publisher);
	
	@Query
	public Publisher getPublisher();
	
	
	@Pre("subject != null #IllegalArgumentException")
	@Pos("getSubject().compare(subject) == 0")
	public void setSubject(Subject subject);
	
	@Query
	public Subject getSubject();
	
	
}
